definitional equality
#Fleeting_Notes
definitional equality
かなり日本語訳が難しいらしい用語
Martin-Löf型理論で出てくる
計算や簡約によって同じものと見なせる等価性を指す
Lean JAのスレッドでまだ結論が出ていない
TARB書評: 飯田隆(編)『知の教科書 論理の哲学』 | Tokyo Academic Review of Books
$ a \equiv b : A
意味: a and b are definitionally equal objects of type A
訳: aとbは型Aに属する定義的に等しい対象
The Type Theory of LeanのP6-7に、Leanのdefinitional equalityの例がある
『The Type Theory of Lean』
確認用
Q. definitional equality
関連
judgmental equality
proof-irrelevance
参考
『Homotopy Type Theory: Univalent Foundations of Mathematics』 P19
メモ
judgmental equality in nLab
調査用
Google.icon definitional equality(日)
Google.icon definitional equality(英)
Wikipedia.icon
definitional equality - Wikipedia(日)
definitional equality(検索) - Wikipedia(日)
Wikipedia.icon
definitional equality - Wikipedia(英)
definitional equality(検索) - Wikipedia(英)